COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002			      The Boyer-Moore Theorem Prover
C00005 ENDMK
C⊗;
		      The Boyer-Moore Theorem Prover

BMP is the Boyer-Moore theorem prover.  This version
is MACLISP with the theorem prover code loaded.
It can be run directly (.r BMP) or as a lisp subjob from E
(⊗x sl BMP).

The SAIL directory for the theorem prover is [BMP,SYS].
All documentation, code and examples reside there.

CODE.DOC contains minimal documentation for the MACLISP version.
The manual for the original (Interlisp) version is contained in 
OLDCOD.DOC.  It is useful for obtaining further information about
some of the commands used in the examples.

A large collection of examples is contained in XXXS.LIS.  They 
are partitioned into calls to the PROVEALL function.
The arguments to PROVEALL are a list of `events', a flag, and a name.
Events are things like note-libs, definitions, declarations, and proofs.  
For example

    (PROVEALL '((BOOT-STRAP)) NIL "BOOT-STRAP")

or 
    (PROVEALL
      '((NOTE-LIB "BOOT-STRAP.LIB" "BOOT-STRAP.LISP")
         ..  other events ..
        )
      NIL "PROVEALL")

Executing a proveall causes the events to be executed and
several files are written:

    name.tty   errors and warnings
    name.pro   running comentary on what BMP is doing
    name.lib  library - to be loaded by note-lib
    name.lis   lisp defuns of functions defined by events in the events-list
       proof loaded by (NOTE-LIB name.lib name.lisp)

Output for the following provalls exist at SAIL

    BOOT-STRAP
    PROVEA
    RSA
    WILSON
    GAUSS